(set-logic QF_S)
(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () String)
(declare-fun var4 () String)
(declare-fun var5 () String)
(declare-fun var6 () String)
(declare-fun var7 () String)
(declare-fun var8 () String)
(declare-fun var9 () String)
(declare-fun var10 () String)
(declare-fun var11 () String)
(declare-fun var12 () String)
(declare-fun var13 () String)
(declare-fun var14 () String)
(declare-fun var15 () String)
(declare-fun var16 () String)
(declare-fun var17 () String)
(declare-fun var18 () String)
(declare-fun var19 () String)
(declare-fun var20 () String)
(declare-fun var21 () String)
(declare-fun var22 () String)
(declare-fun var23 () String)
(declare-fun var24 () String)
(declare-fun var25 () String)
(declare-fun var26 () String)
(declare-fun var27 () String)
(declare-fun var28 () String)
(declare-fun var29 () String)
(declare-fun var30 () String)
(declare-fun var31 () String)
(declare-fun var32 () String)
(declare-fun var33 () String)
(declare-fun var34 () String)
(declare-fun var35 () String)
(declare-fun var36 () String)
(declare-fun var37 () String)
(declare-fun var38 () String)
(declare-fun var39 () String)
(declare-fun var40 () String)
(declare-fun var41 () String)
(declare-fun var42 () String)
(declare-fun var43 () String)
(declare-fun var44 () String)
(declare-fun var45 () String)
(declare-fun var46 () String)
(declare-fun var47 () String)
(declare-fun var48 () String)
(declare-fun var49 () String)
(declare-fun var50 () String)
(declare-fun var51 () String)
(declare-fun var52 () String)
(declare-fun var53 () String)
(declare-fun var54 () String)
(declare-fun var55 () String)
(declare-fun var56 () String)
(declare-fun var57 () String)
(declare-fun var58 () String)
(declare-fun var59 () String)
(declare-fun var60 () String)
(assert (= var0 (str.++ var1 var2)))
(assert (= var2 (str.++ var3 var4)))
(assert (= var4 (str.++ var5 var6)))
(assert (= var6 (str.++ var7 var8)))
(assert (= var8 (str.++ var9 var10)))
(assert (= var10 (str.++ var11 var12)))
(assert (= var12 (str.++ var13 var14)))
(assert (= var14 (str.++ var15 var16)))
(assert (= var16 (str.++ var17 var18)))
(assert (= var18 (str.++ var19 var20)))
(assert (= var20 (str.++ var21 var22)))
(assert (= var22 (str.++ var23 var24)))
(assert (= var24 (str.++ var25 var26)))
(assert (= var26 (str.++ var27 var28)))
(assert (= var28 (str.++ var29 var30)))
(assert (= var30 (str.++ var31 var32)))
(assert (= var32 (str.++ var33 var34)))
(assert (= var34 (str.++ var35 var36)))
(assert (= var36 (str.++ var37 var38)))
(assert (= var38 (str.++ var39 var40)))
(assert (= var40 (str.++ var41 var42)))
(assert (= var42 (str.++ var43 var44)))
(assert (= var44 (str.++ var45 var46)))
(assert (= var46 (str.++ var47 var48)))
(assert (= var48 (str.++ var49 var50)))
(assert (= var50 (str.++ var51 var52)))
(assert (= var52 (str.++ var53 var54)))
(assert (= var54 (str.++ var55 var56)))
(assert (= var56 (str.++ var57 var58)))
(assert (= var58 (str.++ var59 var60)))
(assert (= var0 "solution"))
(assert (= "#" (str.at var40 90)))
(assert (= "u" (str.at var54 85)))
(assert (= ":" (str.at var48 41)))
(assert (= "e" (str.at var52 65)))
(assert (= """" (str.at var30 61)))
(assert (= "M" (str.at var6 51)))
(assert (= "2" (str.at var46 38)))
(assert (= "4" (str.at var9 70)))
(assert (= "0" (str.at var60 44)))
(assert (= "q" (str.at var1 75)))
(assert (= "b" (str.at var8 14)))
(assert (= "r" (str.at var15 57)))
(assert (= "|" (str.at var10 91)))
(assert (= """" (str.at var40 6)))
(assert (= "4" (str.at var55 22)))
(assert (= "[" (str.at var59 55)))
(assert (= "h" (str.at var50 48)))
(assert (= "&" (str.at var60 4)))
(assert (= "/" (str.at var53 36)))
(assert (= "8" (str.at var34 44)))
(assert (= "3" (str.at var60 69)))
(assert (= "4" (str.at var54 7)))
(assert (= "w" (str.at var27 17)))
(assert (= "v" (str.at var22 49)))